M:MsgA, k:Knd, s:M.state, v:M.da(k). M.sends(k,s,v)  (M.Msg List) 

latex

Definitions	x:A. B(x), M.state, M.da(a), t  T, M.Msg, M.sends(k,s,v), t.2, t.1, x. t(x), Msg(da), P  Q, P & Q, P  Q, x(s1,s2), MsgA, , x(s), P  Q, Valtype(da;k)
Lemmas	concat wf, ma-Msg wf, map wf, Knd wf, IdLnk wf, assert wf, Id wf, ma-state wf, ma-valtype wf, pi1 wf, fpf-cap wf, Kind-deq wf, rcv wf, pi2 wf, fpf-vals wf, product-deq wf, idlnk-deq wf, eqof wf, top wf, msga wf, deq property, tagged-messages wf, subtype rel list, Msg wf, mlnk wf